Search for: All records

User authentication systems based on cardiovascular biosignals have gained prominence in recent years, as these signals are presumed to be difficult to forge. We challenge this assumption by showing that an observer who has access to one type of cardiac data --- such as a user's pulse waveform, readily obtainable from video and commercial smartwatches --- can design a spoofing attack strong enough to fool authentication systems based on other cardiovascular biosignals. We present BioForge, an approach that leverages a cycle-consistent generative adversarial network to synthesize realistic physiological signals for a given user without relying on simultaneously collected supervision data. We evaluate BioForge on multiple open-access datasets and an array of verification systems, many of which can be fooled over 50% of the time in 10 or fewer attempts. Notably, we are able to fool systems that rely not just on heart rate and peak locations but also on the morphology of the waveforms. We additionally showcase how BioForge can be used to spoof authentication systems from biosignal data extracted from video clips of a target user. Our work demonstrates that authentication systems should not rely on the secrecy of cardiovascular biosignals. 

Reactis® is a suite of tools produced by Reactive Systems, Inc. (RSI), for automated test generation from, and verification of, sys- tems given in either the modeling languages MATLAB® / Simulink® / Stateflow® of The MathWorks, Inc., or ANSI C. RSI was founded by three of the authors of this paper in 1999, with the first release of Reactis coming in 2002; the tools are used in the testing and validation of embed- ded control systems in a variety of industries, including automotive and aerospace / defense. This paper traces the development of the Reactis tool suite from earlier research on model-checking tools undertaken by the authors and others, highlighting the importance of both the foun- dational basis of Reactis and the essential adaptations and extensions needed for a commercially successful product. 

We present Grapple, a new and powerful framework for explicit-state model checking on GPUs. Grapple is based on swarm verification (SV), a model-checking technique wherein a collection or swarm of small, memory- and time-bounded verification tests (VTs) are run in parallel to perform state-space exploration. SV achieves high state-space coverage via diversification of the search strategies used by constituent VTs. Grapple represents a swarm implementation for the GPU. In particular, it runs a parallel swarm of internally-parallel VTs, which are implemented in a manner that specifically targets the GPU architecture and the SIMD parallelism its computing cores offer. Grapple also makes effective use of the GPU shared memory, eliminating costly inter-block communication overhead. We conducted a comprehensive performance analysis of Grapple focused on the various design parameters, including the size of the queue structure, implementation of guard statements, and nondeterministic exploration order. Tests are run with multiple hardware configurations, including on the Amazon cloud. Our results show that Grapple performs favorably compared to the SPIN swarm and a prior non-swarm GPU implementation. Although a recently debuted FPGA swarm is faster, the deployment process to the FPGA is much more complex than Grapple's.